(defprop trans2 (
 TRANSFORM
 TRANSA
 INST
 ISVAR
 SIDE
 TRANSB
 DZ
 D1
) trans2fns)



(DEFUN TRANSFORM (E R DONE) 
       (COND ((MEMBER E DONE) E)
	     (T ((LAMBDA (W) (COND ((EQ W E)
				    (COND ((ATOM E) E)
					  (T ((LAMBDA (X Y) 
					       (COND
						((AND (EQ X (CAR E))
						      (EQ Y (CDR E)))
						 (SIDE
						  E
						  (SETQ DONE
							(CONS E
							      DONE))))
						(T (TRANSFORM (CONS X Y)
							      R
							      DONE))))
					      (TRANSFORM (CAR E)
							 R
							 DONE)
					      (TRANSFORM (CDR E)
							 R
							 DONE)))))
				   (T (TRANSFORM W R DONE))))
		 (TRANSA E R)))))

(DEFUN TRANSA (E R) 
       (COND ((NULL R) E)
	     (T ((LAMBDA (W) (COND ((EQ W E) (TRANSA E (CDR R)))
				   (T W)))
		 (TRANSB E (CAR R))))))

(DEFUN INST (E PAT ML) 
  (COND ((EQ ML (QUOTE NO)) ML) 
	((ATOM PAT) 
	  (COND ((ISVAR PAT)
		  ((LAMBDA (W) (COND ((NULL W) (CONS (CONS PAT E) ML))
				     ((EQUAL (CDR W) E) ML) 
				     (T (QUOTE NO)))) 
		   (ASSOC PAT ML)))
		((EQ PAT E) ML) 
		(T (QUOTE NO)))) 
	((ATOM E) (QUOTE NO))
	(T (INST (CDR E) (CDR PAT) (INST (CAR E) (CAR PAT) ML)))))

(DEFUN ISVAR (V) (MEMQ V '(X Y Z)))


(DEFUN SIDE (X Y) X)

(DEFUN TRANSB (E RULE) 
       ((LAMBDA (W) 
	   (COND ((EQ W 'NO) E)
		 ((NOT (EVAL (SUBLIS W (CADR RULE))))  E)
	         ((CADDR RULE) (PRINT E) (PRINT RULE) 
			       (PRINT (SETQ E (SUBLIS W ( CADDDR RULE)))) (TERPRI) E )
		 (T (PRINT E) (PRINT RULE) 
			      (PRINT (SETQ E (EVAL (SUBLIS W (CADDDR RULE)))))(TERPRI) E) ))
	(INST E (CAR RULE) NIL)))

(SETQ R1 '(((PLUS . X) (MEMBER 0 'X) NIL (CONS 'PLUS (DZ 'X)))
	   ((TIMES . X) (MEMBER 0 'X) T 0)
	   ((TIMES . X) (MEMBER 1 'X) NIL (CONS 'TIMES (D1 'X)))
	   ((PLUS) T T 0)
	   ((PLUS X) T T X)
	   ((TIMES) T T 1)
	   ((TIMES X) T T X)))

(DEFUN DZ (U) 
       (COND ((NULL U) NIL)
	     ((EQ (CAR U) 0) (DZ (CDR U)))
	     ((AND (NOT (ATOM (CAR U))) (EQ (CAAR U) 'PLUS))
	      (APPEND (CDAR U) (DZ (CDR U))))
	     (T (CONS (CAR U) (DZ (CDR U))))))

(DEFUN D1 (U) 
       (COND ((NULL U) NIL)
	     ((EQ (CAR U) 1) (D1 (CDR U)))
	     ((AND (NOT (ATOM (CAR U))) (EQ (CAAR U) 'TIMES))
	      (APPEND (CDAR U) (D1 (CDR U))))
	     (T (CONS (CAR U) (D1 (CDR U)))))) 
;;; SAMPLE RUN

;;;(SETQ E1 (DIFF (QUOTE (TIMES X (PLUS Y 1) 3)) (QUOTE X)) )

;;;(PLUS (TIMES 1 (PLUS Y 1) 3) (TIMES X (PLUS 0 0) 3) (TIMES X (PLUS Y 1) 0)) 

;;;(TRANSFORM E1 R1 NIL) 
;;;(TIMES (PLUS Y 1) 3)